a:Atom1, A:MsgA, s:A.state.
AtomFree(ds(A))
 AtomFree(da(A))
 x.A.init(x)?s(x):A.state>>a
 ma-body(A):Shape(A)>>a  s:A.state>>a 

latex

Definitions

t  T, MsgA, AtomFree(T;x), Knd, Type, KindDeq, P  Q, a:A fp B(a), Void, x:T>>a, x:AB(x), Id, f(x)?z, IdDeq, Top, Atom$n, AtomFree(d), M.state, State(ds), Shape(M), M.ds(x), Valtype(da;k), M.init(x)?v, da(M), ds(M), EqDecider(T), left+right, union-deq(A;B;a;b), sumdeq(a;b), sum-deq(A;B;a;b), IdLnk, x:AB(x), IdLnkDeq, product-deq(A;B;a;b), proddeq(a;b), prod-deq(A;B;a;b), Atom, , {x:A| B(x) }, , AB, A, P  Q, False, a<b, #$n, AtomDeq, atom-deq-aux, NatDeq, <a,b>, nat-deq-aux, x.A(x), f(a), xdom(f). v=f(x)   P(x;v), x:A. B(x), type List, (x  l), x:A. B(x), A & B, ||as||, s = t, l[i], hd(l), Case of a; nil  s ; x.y, rec:z  t(x;y;z), nil, nth_tl(n;as), if b t else f fi, Case b of inl(x)  s(x) ; inr(y)  t(y), x  dom(f), deq-member(eq;x;L), reduce(f;k;as), false, inr(x), , *, 1of(t), f(x), 2of(t), A/x,y. B(x;y), x. t(x), x:A. B(x), Unit, P  Q, P & Q, Prop, , b, b, {T}, ma-body(M), MsgA(ds;da), P  Q, locl(a), rcv(l,tg)

Lemmas

IdLnk wf, pi2 wf, rcv wf, pi1 wf, ma-state wf, locl wf, pair-inherence, atom-free-ma-shape, ma-body wf, ma-shape wf, inherence-trivial, fpf-ap wf, subtype rel self, assert wf, not wf, bnot wf, bool wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf wf, fpf-cap wf, top wf, inherence-ap-elim, atom-free-Knd, Knd wf, Kind-deq wf, atom-free-fpf, atom-free-Id, Id wf, id-deq wf, ma-init-val wf, ma-st wf, inheres wf, atom-free-ma-state, ma da wf, atom-free-decl wf, ma ds wf, msga wf